package model.sequent.tokens;

import java.util.HashSet;
import java.util.Set;

/**
 * Represents a sequent tree. Contains two sets: one for the 'true' side of the sequent and one for the 'false' side of the sequent.
 * 
 * @author Karen Berntsen (s0815799)
 * @author Erik Stens (s0615374)
 */
public class Sequent implements Cloneable {
	private Set<Expression>	trueExpressionSet	= new HashSet<Expression>();
	private Set<Expression>	falseExpressionSet	= new HashSet<Expression>();
	
	public Sequent() {}
	
	public Sequent(Expression trueExpression, Expression falseExpression) {
		addTrueExpression(trueExpression);
		addFalseExpression(falseExpression);
	}
	
	public Sequent(Sequent sequentA, Sequent sequentB) {
		trueExpressionSet.addAll(sequentA.trueExpressionSet);
		trueExpressionSet.addAll(sequentB.trueExpressionSet);
		falseExpressionSet.addAll(sequentA.falseExpressionSet);
		falseExpressionSet.addAll(sequentB.falseExpressionSet);
	}
	
	public Sequent(Set<Expression> trueExpressionSet, Set<Expression> falseExpressionSet) {
		this.trueExpressionSet = trueExpressionSet;
		this.falseExpressionSet = falseExpressionSet;
	}
	
	public void addTrueExpression(Expression expression) {
		if (expression != null) {
			trueExpressionSet.add(expression);
		}
	}
	
	public void addFalseExpression(Expression expression) {
		if (expression != null) {
			falseExpressionSet.add(expression);
		}
	}
	
	public void removeTrueExpression(Expression expression) {
		if (expression != null) {
			trueExpressionSet.remove(expression);
		}
	}
	
	public void removeFalseExpression(Expression expression) {
		if (expression != null) {
			falseExpressionSet.remove(expression);
		}
	}
	
	public Set<Expression> getTrueExpressionSet() {
		return trueExpressionSet;
	}
	
	public Set<Expression> getFalseExpressionSet() {
		return falseExpressionSet;
	}
	
	/**
	 * @return a String representing the sequent tree.
	 */
	@Override
	public String toString() {
		StringBuilder sb = new StringBuilder();
		
		appendExpressionSet(sb, falseExpressionSet);
		
		sb.append("@\n\n");
		
		appendExpressionSet(sb, trueExpressionSet);
		
		return sb.toString();
	}
	
	private void appendExpressionSet(StringBuilder sb, Set<Expression> expressionSet) {
		boolean first = true;
		for (Expression expression : expressionSet) {
			if (!first) {
				sb.append("\t,\n\n");
			}
			appendExpression(sb, expression, 2);
			first = false;
		}
	}
	
	private void appendExpression(StringBuilder sb, Expression expression, int depth) {
		if (expression instanceof Atom) {
			Atom atom = (Atom) expression;
			
			appendTabs(sb, depth);
			sb.append(atom.getName() + "\n\n");
		} else if (expression instanceof BiOperatorExpression) {
			BiOperatorExpression boe = (BiOperatorExpression) expression;
			
			appendExpression(sb, boe.getRightExpression(), depth + 1);
			
			appendTabs(sb, depth);
			sb.append(boe.getOperator().toString() + "\n\n");
			
			appendExpression(sb, boe.getLeftExpression(), depth + 1);
		} else if (expression instanceof SimpleOperatorExpression) {
			SimpleOperatorExpression soe = (SimpleOperatorExpression) expression;
			
			appendExpression(sb, soe.getExpression(), depth + 1);
			
			appendTabs(sb, depth);
			sb.append(soe.getOperator().toString() + "\n\n");
		} else {
			throw new RuntimeException("Expressiontype is not supported");
		}
	}
	
	private void appendTabs(StringBuilder sb, int nTabs) {
		for (int i = 0; i < nTabs; i++) {
			sb.append('\t');
		}
	}
	
	@Override
	public int hashCode() {
		return trueExpressionSet.hashCode() ^ falseExpressionSet.hashCode();
	}
	
	/**
	 * @return true if this sequent is equal to the argument sequent.
	 */
	@Override
	public boolean equals(Object o) {
		if (o instanceof Sequent) {
			Sequent sequent = (Sequent) o;
			
			if (trueExpressionSet.equals(sequent.trueExpressionSet) && falseExpressionSet.equals(sequent.falseExpressionSet)) {
				return true;
			}
			
			// A sequent is commutative, though this gave some problems in the dynamic programming part of the evaluator, so this part is commented.
			// return trueExpressionSet.equals(sequent.falseExpressionSet) && falseExpressionSet.equals(sequent.trueExpressionSet);
		}
		return false;
	}
	
	@Override
	public Sequent clone() {
		Set<Expression> newTrueExpressionSet = new HashSet<Expression>();
		Set<Expression> newFalseExpressionSet = new HashSet<Expression>();
		
		for (Expression expression : trueExpressionSet) {
			newTrueExpressionSet.add(expression.clone());
		}
		
		for (Expression expression : falseExpressionSet) {
			newFalseExpressionSet.add(expression.clone());
		}
		
		return new Sequent(newTrueExpressionSet, newFalseExpressionSet);
	}
	
	public boolean onlyAtoms() {
		for (Expression expression : trueExpressionSet) {
			if (!(expression instanceof Atom)) {
				return false;
			}
		}
		
		for (Expression expression : falseExpressionSet) {
			if (!(expression instanceof Atom)) {
				return false;
			}
		}
		
		return true;
	}
}